$\forall$${\it es}$:event\_system\{i:l\}, ${\it as}$,${\it bs}$:(es{-}E(${\it es}$) List).
\\[0ex]loc{-}ordered(${\it es}$; ${\it as}$)
\\[0ex]$\Rightarrow$ loc{-}ordered(${\it es}$; ${\it bs}$)
\\[0ex]$\Rightarrow$ ((${\it as}$ = ${\it bs}$) $\Leftarrow\!\Rightarrow$ ($\forall$$e$:es{-}E(${\it es}$). ($e$ $\in$ ${\it as}$) $\Leftarrow\!\Rightarrow$ ($e$ $\in$ ${\it bs}$)))